let A be preIfWhileAlgebra; :: thesis: for S being non empty set
for T being Subset of S holds
( pr1 S,the carrier of A is complying_with_empty-instruction & pr1 S,the carrier of A is complying_with_catenation & pr1 S,the carrier of A complies_with_if_wrt T & pr1 S,the carrier of A complies_with_while_wrt T )
let S be non empty set ; :: thesis: for T being Subset of S holds
( pr1 S,the carrier of A is complying_with_empty-instruction & pr1 S,the carrier of A is complying_with_catenation & pr1 S,the carrier of A complies_with_if_wrt T & pr1 S,the carrier of A complies_with_while_wrt T )
let T be Subset of S; :: thesis: ( pr1 S,the carrier of A is complying_with_empty-instruction & pr1 S,the carrier of A is complying_with_catenation & pr1 S,the carrier of A complies_with_if_wrt T & pr1 S,the carrier of A complies_with_while_wrt T )
set f = pr1 S,the carrier of A;
thus for s being Element of S holds (pr1 S,the carrier of A) . s,(EmptyIns A) = s by FUNCT_3:def 5; :: according to AOFA_000:def 28 :: thesis: ( pr1 S,the carrier of A is complying_with_catenation & pr1 S,the carrier of A complies_with_if_wrt T & pr1 S,the carrier of A complies_with_while_wrt T )

hereby :: according to AOFA_000:def 29 :: thesis: ( pr1 S,the carrier of A complies_with_if_wrt T & pr1 S,the carrier of A complies_with_while_wrt T )

let s be Element of S; :: thesis: for I1, I2 being Element of A holds (pr1 S,the carrier of A) . s,(I1 \; I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,I1),I2
let I1, I2 be Element of A; :: thesis: (pr1 S,the carrier of A) . s,(I1 \; I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,I1),I2
thus (pr1 S,the carrier of A) . s,(I1 \; I2) = s by FUNCT_3:def 5
.= (pr1 S,the carrier of A) . s,I1 by FUNCT_3:def 5
.= (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,I1),I2 by FUNCT_3:def 5 ; :: thesis: verum

end;

hereby :: according to AOFA_000:def 30 :: thesis: pr1 S,the carrier of A complies_with_while_wrt T

let s be Element of S; :: thesis: for C, I1, I2 being Element of A holds
( ( (pr1 S,the carrier of A) . s,C in T implies (pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I1 ) & ( (pr1 S,the carrier of A) . s,C nin T implies (pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I2 ) )
let C, I1, I2 be Element of A; :: thesis: ( ( (pr1 S,the carrier of A) . s,C in T implies (pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I1 ) & ( (pr1 S,the carrier of A) . s,C nin T implies (pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I2 ) )
(pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = s by FUNCT_3:def 5
.= (pr1 S,the carrier of A) . s,C by FUNCT_3:def 5 ;
hence ( ( (pr1 S,the carrier of A) . s,C in T implies (pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I1 ) & ( (pr1 S,the carrier of A) . s,C nin T implies (pr1 S,the carrier of A) . s,(if-then-else C,I1,I2) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I2 ) ) by FUNCT_3:def 5; :: thesis: verum

end;

let s be Element of S; :: according to AOFA_000:def 31 :: thesis: for C, I being Element of A holds
( ( (pr1 S,the carrier of A) . s,C in T implies (pr1 S,the carrier of A) . s,(while C,I) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I),(while C,I) ) & ( (pr1 S,the carrier of A) . s,C nin T implies (pr1 S,the carrier of A) . s,(while C,I) = (pr1 S,the carrier of A) . s,C ) )
let C, I be Element of A; :: thesis: ( ( (pr1 S,the carrier of A) . s,C in T implies (pr1 S,the carrier of A) . s,(while C,I) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I),(while C,I) ) & ( (pr1 S,the carrier of A) . s,C nin T implies (pr1 S,the carrier of A) . s,(while C,I) = (pr1 S,the carrier of A) . s,C ) )
(pr1 S,the carrier of A) . s,C = s by FUNCT_3:def 5;
hence ( ( (pr1 S,the carrier of A) . s,C in T implies (pr1 S,the carrier of A) . s,(while C,I) = (pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . ((pr1 S,the carrier of A) . s,C),I),(while C,I) ) & ( (pr1 S,the carrier of A) . s,C nin T implies (pr1 S,the carrier of A) . s,(while C,I) = (pr1 S,the carrier of A) . s,C ) ) by FUNCT_3:def 5; :: thesis: verum